step(al,bs,tm(s,[ctxm(xi_,u,ip,ip_al_4,ip_al_4),ctxm(xi_,sp,ip,ip_bs,ip_bs)],pri(enc,[ctxm(xi_,u,i_sess,ss(xi_,i_sess),ss(xi_,i_sess)),pri(aka,[ctxm(xi_,dot,kM_c,kM_c,kM_c),ctxm(xi_,dot,n_a,ss(xi_,i_n_a),ss(xi_,c_n_a)),ctxm(xi_,sp,kM,kM_bs,kM_bs),ctxm(xi_,dot,n_b,ss(xi_,i_n_b),ss(xi_,c_n_b))])]))).
